HOL
The HOL theorem prover Please edit this page or contact Jonathan Bowen if you know of relevant online information not included here. ---- This document contains some pointers to information on the HOL mechanical theorem proving system, based on , available around the world on the World Wide Web (WWW). ---- The following on-line information is available: * The HOL System. Information provided by the Automated Reasoning Group at the University of Cambridge Computer Laboratory, UK. See also FTP archive. * HOL 4 and Project information — HOL theorem-proving system from SourceForge. * HOL documentation at Brigham Young University (second sourced in the UK). * The sources for the HOL system (with an index) at the University of Cambridge Computer Laboratory (second sourced in the US). * Archive material including papers and contributed software for HOL (with a README file) are available. * Release Note for HOL from the Automated Reasoning Group at Cambridge. * The info-hol electronic mailing list enables discussion on topics concerning HOL and includes announcements of HOL meetings. Contact [mailto:info-hol-request@lal.cs.byu.edu info-hol-request@lal.cs.byu.edu] to be added to the list. The archives are searchable and there is a list of subscribers. * Conferences related to the HOL System. See TPHOLs'98: International Conference on Theorem Proving in Higher Order Logics, Canberra, Australia, 21 September – 2 October 1998. * The HOL2000 initiative is trying to put together a design for the next generation of HOL-like theorem proving environments. To join the discussion list, email [mailto:hol2000-request@lal.cs.byu.edu hol2000-request@lal.cs.byu.edu]. * Some support for the Z notation is available as documented in the paper [ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/zhol.ps.Z Z and HOL]. The source files for various Z specifications in HOL are available. * ProofPower is a commercial tool, developed and marketed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z. * HOL-Z tool. A shallow embedding of the Z notation in the higher-order logic theorem prover Isabelle, similar to that of the HOL system. Also mirrored here and here. * Information on the HOL Theorem Prover from the Formal Methods and Theory Group at Glasgow. ]] * A good introductory book is ''Introduction to HOL: A theorem proving environment for higher order logic, edited by M.J.C. Gordon and T.F. Melham, 1993. ISBN 0-521-44189-7. See also: ** Publisher's information from Cambridge University Press. ISBN 0-521-44189-7. ** A book review of ``An introduction to HOL'' by Graham Hutton. ** Order from Amazon USA or Amazon UK. * Higher Order Logic theorem provers pointers from Yahoo. * CHOL distribution from INRIA, an attempt to privide a better user interface for HOL using the Centaur system. * Higher Order Logic Theorem Proving and its Applications special issue of The Computer Journal by Tom Melham. * HOL Light by John Harrison. See also PVS, another newer theorem proving tool based on higher order logic. ---- Last updated by Jonathan Bowen, 24 March 2009. Further information for possible inclusion is welcome. Category:HOL Category:Theorem provers Category:Virtual Library